decl{-}type\{i:l\}(${\it ds}$; $x$) $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$fpf{-}cap(${\it ds}$;IdDeq;$x$;Void)